Polymorphic type inference and assignment
要約
MLの多相型に参照を導入したとき型安全性を失わないようにする
関数によってbypassされる型変数を記録する
Introduction
多相型は副作用のない体系にはぴったりはまる
副作用のある手続き型言語などに持ち込むと問題が発生する
例
code:example_problematic.ml
let r = ref [] in (* (1) *)
if head(!r) then ... else ... (* (3) *)
rにナイーブにforall 'a. 'a list refなる型を与えてみる (1)
rをint list refとして[1]を代入する (2)
rをbool list refとして条件節で使う (3)
well-typedだけど型安全でない!
多相的かつmutableな(in-placeで変更がある)データの利用を制限しなければならない
わかりやすい解決策の1つ
mutableなデータ構造にすべて単相的な型を与える
まあ問題は解決するけど
mutableな値を返す多相的な関数を書くことができない
かなしいね
↑の欠点
genericな(破壊的変更を要する)ほとんどのデータ構造を効率的に実装できない
多相的かつmutableな値を使うことが禁止されている
内部的な計算のみに使うときでさえも
例
code:example_internal.ml
(* 非破壊的なmap function *)
let rec applicative_map f l =
if null l then [] else
f (head l) :: applicative_map f (tail l)
(* 破壊的なmap function *)
let imperative_map f l =
let argument = ref l and result = ref [] in
while not (null !argument) do
result := f (head !argument) :: !result;
argument := tail !argument
done;
reverse !result
型システムによっては
imperative_mapがill-typedであるとしてrejectされる
applicative_mapよりも制約のある型が付く
プログラミングスタイルによって型への制約がかかってしまう
用語
type variableがdangerousである
参照型に自由に出現する
we never generalize a type variable that may be free in the type of a reference. Such a type variable is said to be dangerous.
記法
$ A \triangleright L
型Aのオブジェクトは型Lの環境に出現することが許されている